a:, n:. (a  n)   

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), , False, P  Q, A, a  b  T , , P & Q, A  B, , P  Q, P  Q, S  T
Lemmas	nat wf, nat plus wf, le to lt, mul cancel in lt, nat plus inc int nzero, div rem sum, add functionality wrt lt, rem bounds 1, le wf